Prof. Dr. Herbert Klaeren

Semantik von Programmiersprachen (V3+Ü2)

Termin

variabel

Turnus

Unregelmäßig (Sommersemester)

Prüfungsfach

Theoretische Informatik

Stichworte

Die Vorlesung ist eine Einführung in die Werkzeuge der formalen Semantik. Die Definition einer Semantik ist notwendig, um das Verhalten von Programmen eindeutig festzulegen, die Konsistenz von Programmiersprachen sicherzustellen und Voraussetzungen für Korrektheitsbeweise von Programmen und Compilern zu schaffen. Die Kenntnisse aus der Vorlesung sind auch in anderen Veranstaltungen von Nutzen, insbesondere im Compilerbau, in der Anwendung von Programmiersprachen und im parallelen Rechnen.

Nach einer Motivation und Einführung mit Wiederholung der mathematischen Grundkenntnisse beschäftigt sich die Vorlesung zunächst mit den Grundlagen aus der universellen Algebra, insbesondere der Bereichstheorie und in Verbindung daran mit der Semantik von Typen. Verschiedene Formen von Semantik-Definitionen werden betrachtet, mit Schwerpunkt auf der denotationellen Semantik. Im Rahmen davon wird betrachtet, wie sich die meist ``natürlichsprachlich'' formulierten Semantiken von Programmiersprachen in Beziehung setzen lassen mit einer natürlichen Semantik, einer denotationellen Semantik und einer Implementierung.

Ziel der Vorlesung ist es, die nötige Motivation und die Fähigkeiten zu schaffen, formale Semantik verstehen und damit umgehen zu können, und etwas von den Vorbehalten vor algebraischen Methoden und mathematischer Notation auszuräumen.

Voraussetzungen

Grundstudium Informatik. Kenntnisse aus ``Konzepte von Programmiersprachen'', ``Compilerbau'', ``Lambda-Kalkül'', ``Logik für Informatiker'' oder ``Funktionale Programmierung'' sind willkommen, aber nicht Voraussetzung. Die nötigen Kenntnisse aus Algebra und Logik werden vermittelt.

Literatur

Prof. Herbert Klaeren
Last modified: Mon May 12 17:37:33 MES